Issue690a.agda:8,1-9,14
T is not strictly positive, because it occurs
in an index of the target type of the constructor c
in the definition of T.
